app2(app2(app2(if, true), x), y) -> x
app2(app2(app2(if, true), x), y) -> y
app2(app2(takeWhile, p), nil) -> nil
app2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(takeWhile, p), xs))), nil)
app2(app2(dropWhile, p), nil) -> nil
app2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(dropWhile, p), xs)), app2(app2(cons, x), xs))
↳ QTRS
↳ DependencyPairsProof
app2(app2(app2(if, true), x), y) -> x
app2(app2(app2(if, true), x), y) -> y
app2(app2(takeWhile, p), nil) -> nil
app2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(takeWhile, p), xs))), nil)
app2(app2(dropWhile, p), nil) -> nil
app2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(dropWhile, p), xs)), app2(app2(cons, x), xs))
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(dropWhile, p), xs)
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(if, app2(p, x)), app2(app2(dropWhile, p), xs))
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(takeWhile, p), xs))), nil)
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(p, x)
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(takeWhile, p), xs)))
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(if, app2(p, x))
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(app2(if, app2(p, x)), app2(app2(dropWhile, p), xs)), app2(app2(cons, x), xs))
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(takeWhile, p), xs)
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(if, app2(p, x))
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(p, x)
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(cons, x), app2(app2(takeWhile, p), xs))
app2(app2(app2(if, true), x), y) -> x
app2(app2(app2(if, true), x), y) -> y
app2(app2(takeWhile, p), nil) -> nil
app2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(takeWhile, p), xs))), nil)
app2(app2(dropWhile, p), nil) -> nil
app2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(dropWhile, p), xs)), app2(app2(cons, x), xs))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(dropWhile, p), xs)
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(if, app2(p, x)), app2(app2(dropWhile, p), xs))
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(takeWhile, p), xs))), nil)
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(p, x)
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(takeWhile, p), xs)))
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(if, app2(p, x))
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(app2(if, app2(p, x)), app2(app2(dropWhile, p), xs)), app2(app2(cons, x), xs))
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(takeWhile, p), xs)
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(if, app2(p, x))
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(p, x)
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(cons, x), app2(app2(takeWhile, p), xs))
app2(app2(app2(if, true), x), y) -> x
app2(app2(app2(if, true), x), y) -> y
app2(app2(takeWhile, p), nil) -> nil
app2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(takeWhile, p), xs))), nil)
app2(app2(dropWhile, p), nil) -> nil
app2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(dropWhile, p), xs)), app2(app2(cons, x), xs))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(dropWhile, p), xs)
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(p, x)
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(takeWhile, p), xs)
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(p, x)
app2(app2(app2(if, true), x), y) -> x
app2(app2(app2(if, true), x), y) -> y
app2(app2(takeWhile, p), nil) -> nil
app2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(takeWhile, p), xs))), nil)
app2(app2(dropWhile, p), nil) -> nil
app2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(dropWhile, p), xs)), app2(app2(cons, x), xs))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(p, x)
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(p, x)
Used ordering: Combined order from the following AFS and order.
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(dropWhile, p), xs)
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(takeWhile, p), xs)
app1 > takeWhile
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(dropWhile, p), xs)
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(takeWhile, p), xs)
app2(app2(app2(if, true), x), y) -> x
app2(app2(app2(if, true), x), y) -> y
app2(app2(takeWhile, p), nil) -> nil
app2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(takeWhile, p), xs))), nil)
app2(app2(dropWhile, p), nil) -> nil
app2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(dropWhile, p), xs)), app2(app2(cons, x), xs))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(takeWhile, p), xs)
app2(app2(app2(if, true), x), y) -> x
app2(app2(app2(if, true), x), y) -> y
app2(app2(takeWhile, p), nil) -> nil
app2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(takeWhile, p), xs))), nil)
app2(app2(dropWhile, p), nil) -> nil
app2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(dropWhile, p), xs)), app2(app2(cons, x), xs))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
APP2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(takeWhile, p), xs)
app1 > APP1 > takeWhile
cons > takeWhile
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
app2(app2(app2(if, true), x), y) -> x
app2(app2(app2(if, true), x), y) -> y
app2(app2(takeWhile, p), nil) -> nil
app2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(takeWhile, p), xs))), nil)
app2(app2(dropWhile, p), nil) -> nil
app2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(dropWhile, p), xs)), app2(app2(cons, x), xs))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(dropWhile, p), xs)
app2(app2(app2(if, true), x), y) -> x
app2(app2(app2(if, true), x), y) -> y
app2(app2(takeWhile, p), nil) -> nil
app2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(takeWhile, p), xs))), nil)
app2(app2(dropWhile, p), nil) -> nil
app2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(dropWhile, p), xs)), app2(app2(cons, x), xs))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
APP2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> APP2(app2(dropWhile, p), xs)
app1 > APP1 > dropWhile
cons > dropWhile
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
app2(app2(app2(if, true), x), y) -> x
app2(app2(app2(if, true), x), y) -> y
app2(app2(takeWhile, p), nil) -> nil
app2(app2(takeWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(takeWhile, p), xs))), nil)
app2(app2(dropWhile, p), nil) -> nil
app2(app2(dropWhile, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(dropWhile, p), xs)), app2(app2(cons, x), xs))